-
Notifications
You must be signed in to change notification settings - Fork 134
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Examples of finite presentations of CommAlgebra's #680
Conversation
Strange... I have no good idea why it's so slow. Did you try making some parts abstract in order to isolate where the slowness is coming from? |
I'm not sure if I tried that. |
Hm. Now it seems to be a lot faster with an abstract 'makeFPAlgebra'... Thanks! |
…te-presentations # Conflicts: # Cubical/Algebra/CommAlgebra/FPAlgebra.agda
Isomorphism between spectrum (understood as zero locus of generators) and comm algebra homomorphisms.
Polynomial algebras are finitely presented
Improve notation
Spec Iso in FPAlgebra.agda
# Conflicts: # Cubical/Algebra/CommAlgebra/Base.agda # Cubical/Algebra/CommAlgebra/FPAlgebra.agda # Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda # Cubical/Algebra/CommAlgebra/Ideal.agda # Cubical/Algebra/CommAlgebra/Instances/Initial.agda # Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda # Cubical/Algebra/CommRing/Ideal.agda
# Conflicts: # Cubical/Algebra/RingSolver/Examples.agda
This reverts commit befff8a.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
small comments
The goal of this PR is, to introduce the notion of a finite presentation (instead of just the Prop 'finitelyPresented') and construct some basic finite presentations.
However, I'm stuck here because of a type checking speed issue. It seems that plugging the algebra
makeFPAlgebra n relations
intoCommAlgebraEquiv
is the cause of the slowdown. Maybe because the fields of this more complicated CommAlgebra get expanded? I don't know...